Nuprl Lemma : comb_for_pi1_wf
2,24
postcript
pdf
(
A
,
B
,
p
,
z
. 1of(
p
))
A
:Type
B
:(
A
Type)
a
:
A
B
(
a
)
True
A
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
,
x
(
s
)
Lemmas
true
wf
,
squash
wf
,
pi1
wf
origin
A,B,p,z. 1of(p)) 
A:Type
B:(AType)a:A
B(a)
TrueA A,B,p,z. 1of(p)) A:TypeB:(AType)a:AB(a)TrueA T
x:A. B(x) T